0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 187 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 5 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
reverseB_in_ga([], []) → reverseB_out_ga([], [])
reverseB_in_ga(.(T36, []), .(T36, [])) → reverseB_out_ga(.(T36, []), .(T36, []))
reverseB_in_ga(.(T70, .(T69, [])), .(T69, .(T70, []))) → reverseB_out_ga(.(T70, .(T69, [])), .(T69, .(T70, [])))
reverseB_in_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, [])))) → reverseB_out_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, []))))
reverseB_in_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, []))))) → reverseB_out_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, [])))))
reverseB_in_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, [])))))) → reverseB_out_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, []))))))
reverseB_in_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, []))))))) → reverseB_out_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, [])))))))
reverseB_in_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, [])))))))) → reverseB_out_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, []))))))))
reverseB_in_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → U2_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccA_in_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, [])))))))))
revaccA_in_gagg([], .(T460, T461), T460, T461) → revaccA_out_gagg([], .(T460, T461), T460, T461)
revaccA_in_gagg(.(T472, T473), T477, T475, T476) → U1_gagg(T472, T473, T477, T475, T476, revaccA_in_gagg(T473, T477, T472, .(T475, T476)))
U1_gagg(T472, T473, T477, T475, T476, revaccA_out_gagg(T473, T477, T472, .(T475, T476))) → revaccA_out_gagg(.(T472, T473), T477, T475, T476)
U2_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccA_out_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, []))))))))) → reverseB_out_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
reverseB_in_ga([], []) → reverseB_out_ga([], [])
reverseB_in_ga(.(T36, []), .(T36, [])) → reverseB_out_ga(.(T36, []), .(T36, []))
reverseB_in_ga(.(T70, .(T69, [])), .(T69, .(T70, []))) → reverseB_out_ga(.(T70, .(T69, [])), .(T69, .(T70, [])))
reverseB_in_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, [])))) → reverseB_out_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, []))))
reverseB_in_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, []))))) → reverseB_out_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, [])))))
reverseB_in_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, [])))))) → reverseB_out_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, []))))))
reverseB_in_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, []))))))) → reverseB_out_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, [])))))))
reverseB_in_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, [])))))))) → reverseB_out_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, []))))))))
reverseB_in_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → U2_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccA_in_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, [])))))))))
revaccA_in_gagg([], .(T460, T461), T460, T461) → revaccA_out_gagg([], .(T460, T461), T460, T461)
revaccA_in_gagg(.(T472, T473), T477, T475, T476) → U1_gagg(T472, T473, T477, T475, T476, revaccA_in_gagg(T473, T477, T472, .(T475, T476)))
U1_gagg(T472, T473, T477, T475, T476, revaccA_out_gagg(T473, T477, T472, .(T475, T476))) → revaccA_out_gagg(.(T472, T473), T477, T475, T476)
U2_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccA_out_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, []))))))))) → reverseB_out_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421)
REVERSEB_IN_GA(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → U2_GA(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccA_in_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, [])))))))))
REVERSEB_IN_GA(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → REVACCA_IN_GAGG(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, []))))))))
REVACCA_IN_GAGG(.(T472, T473), T477, T475, T476) → U1_GAGG(T472, T473, T477, T475, T476, revaccA_in_gagg(T473, T477, T472, .(T475, T476)))
REVACCA_IN_GAGG(.(T472, T473), T477, T475, T476) → REVACCA_IN_GAGG(T473, T477, T472, .(T475, T476))
reverseB_in_ga([], []) → reverseB_out_ga([], [])
reverseB_in_ga(.(T36, []), .(T36, [])) → reverseB_out_ga(.(T36, []), .(T36, []))
reverseB_in_ga(.(T70, .(T69, [])), .(T69, .(T70, []))) → reverseB_out_ga(.(T70, .(T69, [])), .(T69, .(T70, [])))
reverseB_in_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, [])))) → reverseB_out_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, []))))
reverseB_in_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, []))))) → reverseB_out_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, [])))))
reverseB_in_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, [])))))) → reverseB_out_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, []))))))
reverseB_in_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, []))))))) → reverseB_out_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, [])))))))
reverseB_in_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, [])))))))) → reverseB_out_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, []))))))))
reverseB_in_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → U2_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccA_in_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, [])))))))))
revaccA_in_gagg([], .(T460, T461), T460, T461) → revaccA_out_gagg([], .(T460, T461), T460, T461)
revaccA_in_gagg(.(T472, T473), T477, T475, T476) → U1_gagg(T472, T473, T477, T475, T476, revaccA_in_gagg(T473, T477, T472, .(T475, T476)))
U1_gagg(T472, T473, T477, T475, T476, revaccA_out_gagg(T473, T477, T472, .(T475, T476))) → revaccA_out_gagg(.(T472, T473), T477, T475, T476)
U2_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccA_out_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, []))))))))) → reverseB_out_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421)
REVERSEB_IN_GA(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → U2_GA(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccA_in_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, [])))))))))
REVERSEB_IN_GA(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → REVACCA_IN_GAGG(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, []))))))))
REVACCA_IN_GAGG(.(T472, T473), T477, T475, T476) → U1_GAGG(T472, T473, T477, T475, T476, revaccA_in_gagg(T473, T477, T472, .(T475, T476)))
REVACCA_IN_GAGG(.(T472, T473), T477, T475, T476) → REVACCA_IN_GAGG(T473, T477, T472, .(T475, T476))
reverseB_in_ga([], []) → reverseB_out_ga([], [])
reverseB_in_ga(.(T36, []), .(T36, [])) → reverseB_out_ga(.(T36, []), .(T36, []))
reverseB_in_ga(.(T70, .(T69, [])), .(T69, .(T70, []))) → reverseB_out_ga(.(T70, .(T69, [])), .(T69, .(T70, [])))
reverseB_in_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, [])))) → reverseB_out_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, []))))
reverseB_in_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, []))))) → reverseB_out_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, [])))))
reverseB_in_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, [])))))) → reverseB_out_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, []))))))
reverseB_in_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, []))))))) → reverseB_out_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, [])))))))
reverseB_in_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, [])))))))) → reverseB_out_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, []))))))))
reverseB_in_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → U2_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccA_in_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, [])))))))))
revaccA_in_gagg([], .(T460, T461), T460, T461) → revaccA_out_gagg([], .(T460, T461), T460, T461)
revaccA_in_gagg(.(T472, T473), T477, T475, T476) → U1_gagg(T472, T473, T477, T475, T476, revaccA_in_gagg(T473, T477, T472, .(T475, T476)))
U1_gagg(T472, T473, T477, T475, T476, revaccA_out_gagg(T473, T477, T472, .(T475, T476))) → revaccA_out_gagg(.(T472, T473), T477, T475, T476)
U2_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccA_out_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, []))))))))) → reverseB_out_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421)
REVACCA_IN_GAGG(.(T472, T473), T477, T475, T476) → REVACCA_IN_GAGG(T473, T477, T472, .(T475, T476))
reverseB_in_ga([], []) → reverseB_out_ga([], [])
reverseB_in_ga(.(T36, []), .(T36, [])) → reverseB_out_ga(.(T36, []), .(T36, []))
reverseB_in_ga(.(T70, .(T69, [])), .(T69, .(T70, []))) → reverseB_out_ga(.(T70, .(T69, [])), .(T69, .(T70, [])))
reverseB_in_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, [])))) → reverseB_out_ga(.(T114, .(T113, .(T112, []))), .(T112, .(T113, .(T114, []))))
reverseB_in_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, []))))) → reverseB_out_ga(.(T168, .(T167, .(T166, .(T165, [])))), .(T165, .(T166, .(T167, .(T168, [])))))
reverseB_in_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, [])))))) → reverseB_out_ga(.(T232, .(T231, .(T230, .(T229, .(T228, []))))), .(T228, .(T229, .(T230, .(T231, .(T232, []))))))
reverseB_in_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, []))))))) → reverseB_out_ga(.(T306, .(T305, .(T304, .(T303, .(T302, .(T301, [])))))), .(T301, .(T302, .(T303, .(T304, .(T305, .(T306, [])))))))
reverseB_in_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, [])))))))) → reverseB_out_ga(.(T390, .(T389, .(T388, .(T387, .(T386, .(T385, .(T384, []))))))), .(T384, .(T385, .(T386, .(T387, .(T388, .(T389, .(T390, []))))))))
reverseB_in_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421) → U2_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccA_in_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, [])))))))))
revaccA_in_gagg([], .(T460, T461), T460, T461) → revaccA_out_gagg([], .(T460, T461), T460, T461)
revaccA_in_gagg(.(T472, T473), T477, T475, T476) → U1_gagg(T472, T473, T477, T475, T476, revaccA_in_gagg(T473, T477, T472, .(T475, T476)))
U1_gagg(T472, T473, T477, T475, T476, revaccA_out_gagg(T473, T477, T472, .(T475, T476))) → revaccA_out_gagg(.(T472, T473), T477, T475, T476)
U2_ga(T420, T419, T418, T417, T416, T415, T414, T411, T412, T421, revaccA_out_gagg(T412, T421, T411, .(T414, .(T415, .(T416, .(T417, .(T418, .(T419, .(T420, []))))))))) → reverseB_out_ga(.(T420, .(T419, .(T418, .(T417, .(T416, .(T415, .(T414, .(T411, T412)))))))), T421)
REVACCA_IN_GAGG(.(T472, T473), T477, T475, T476) → REVACCA_IN_GAGG(T473, T477, T472, .(T475, T476))
REVACCA_IN_GAGG(.(T472, T473), T475, T476) → REVACCA_IN_GAGG(T473, T472, .(T475, T476))
From the DPs we obtained the following set of size-change graphs: